structure Prassert = 
struct
  structure A = Assert
   
  fun nullemit str:string = str  

  fun pr_st emit st = 
      let fun pr A.Rf = "R"
	    | pr A.Hp = "H"
	    | pr (A.Upd(st1,e0,e1)) = 
	      let val str_st1 = pr(st1)
		  val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "Upd("^str_st1^", "^str_e0^", "^str_e1^")"
	      end
      in emit (pr(st))
      end

  and pr_exp emit e = 
      let fun pr (A.IntNum(i)) = 
	      if(i<0)
	      then ("(-"^Int.toString(Int.abs(i))^")")
	      else Int.toString(i)
	    | pr (A.Addr(ad)) = 
	      if(ad<0)
	      then ("(-"^Int.toString(Int.abs(ad))^")")
	      else Int.toString(ad)
	    | pr (A.Plus(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^"+"^str_e1^")"
	      end 
	    | pr (A.Minus(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^"-"^str_e1^")"
	      end 
	    | pr (A.Times(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in str_e0^"*"^str_e1
	      end 
	    | pr (A.Sel(st0,e0)) = 
	      let val str_st0 = pr_st nullemit st0
		  val str_e0 = pr_exp nullemit e0
	      in str_st0^"["^str_e0^"]"
	      end
	    | pr A.Eax = "eax"
	    | pr A.Ebx = "ebx"
	    | pr A.Ecx = "ecx"
	    | pr A.Edx = "edx"
	    | pr A.Esi = "esi"
	    | pr A.Edi = "edi"
	    | pr A.Esp = "esp"
	    | pr A.Ebp = "ebp"
	    | pr _ = ""
      in emit (pr e)
      end

  fun pr_etype emit t = 
      let fun pr A.Int = "int"
            | pr A.Label = "addr"
            | pr A.Wild = "_"
      in  emit (pr t)
      end

  fun pr_prop emit pp = 
      let fun pr A.True = "true"
	    | pr (A.Imply(p0,p1)) = 
	      let val str_p0 = pr_prop nullemit p0
		  val str_p1 = pr_prop nullemit p1
	      in str_p0^"->"^str_p1
	      end
	    | pr (A.Not(p0)) = 
	      let val str_p0 = pr_prop nullemit p0
	      in "(~"^str_p0^")"
	      end
	    | pr (A.And(p0,p1)) = 
	      let val str_p0 = pr_prop nullemit p0
		  val str_p1 = pr_prop nullemit p1
	      in "("^str_p0^")/\\("^str_p1^")"
	      end
	    | pr (A.Or(p0,p1)) = 
	      let val str_p0 = pr_prop nullemit p0
		  val str_p1 = pr_prop nullemit p1
	      in "("^str_p0^")\\/("^str_p1^")"
	      end
	    | pr (A.Gt(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")>("^str_e1^")"
	      end
	    | pr (A.Ge(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")>=("^str_e1^")"	      
	      end
	    | pr (A.Lt(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")<("^str_e1^")"	      
	      end
	    | pr (A.Le(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")<=("^str_e1^")"	      
	      end
	    | pr (A.Eq(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")=("^str_e1^")"	      
	      end
	    | pr (A.Ne(e0,e1)) = 
	      let val str_e0 = pr_exp nullemit e0
		  val str_e1 = pr_exp nullemit e1
	      in "("^str_e0^")<>("^str_e1^")"	      
	      end
            | pr (A.Ex((s, t), p)) =
              let val p' = pr_prop nullemit p
                  val t' = pr_etype nullemit t
              in "exists "^s^" : "^t'^", ("^p'^")\n"
              end
            | pr (A.InDom(e, st)) =
              let val e' = pr_exp nullemit e
                  val st' = pr_st nullemit st
              in "hindom ("^ e' ^") ("^st'^")"
              end
      in emit (pr pp)
      end

  fun pr_assert' emit asst (state:A.state) = 
      let val prop = asst state
	  val lamda' = pr_prop nullemit prop
	  val rf = pr_st nullemit (#1 state)
	  val hp = pr_st nullemit (#2 state)
	  val lamda = "#(forall R.forall H."^lamda'^")\n\b("^rf
		      ^")\n\b("^hp^")\n"
      in emit lamda
      end

  fun pr_assert emit asst =
      let val state = (A.Rf,A.Hp)
	  val prop = A_Reduce.red_prop(asst state)
	  val lamda' = pr_prop nullemit prop
	  val lamda = "#(forall R.forall H."^lamda'^")\n"
      in emit lamda
      end
  
  fun premit str:string = (print(str);"")

  fun pr_asst asst = pr_assert nullemit asst
  
end
